(include-book "../src/acl2/command-parser")
(include-book "doublecheck" :dir :teachpacks)
;;;Tests for the Command Parser. The command 
;;;parser is so IO-based that tests for it are
;;;going to be pretty sparse -- it essentially
;;;reads in a list of words and calls functions
;;;based on those.


;;helper function for property tests
;;Takes a list of lists and returns one list
;;of all the lists appended together in order,
;;with a delimiter between all the elements
;;but no delimiter at the end.
(defun append-all-with-delim (xss delim)
  (if (consp xss)
      (append (car xss) (if (cdr xss) (list delim) nil)
      	 (append-all-with-delim (cdr xss) delim))
      nil))

;;Generate a random character that is
;;not a newline.
(defrandom random-non-newline-char ()
  (let* ((chr (random-char)))
    (if (member-equal chr
                      (list #\return #\newline ))       
        #\x
        chr)))

;;Test that the command parser's tokenize function
;;splits commands on newlines, but not on spaces.
(defproperty test-tokenizer
	(words :value (random-list-of (cons (random-non-newline-char)
                                             (random-list-of (random-non-newline-char)))))
	(let* ((words-cat (append-all-with-delim words #\newline)))
		(equal (command-tokenizer* words-cat) words)))


